Search for: All records

It is notoriously difficult to verify that a network is behaving as intended, especially at scale. This paper presents Hydra, a system that uses ideas from runtime verification to check that every packet is correctly processed with respect to a specification in real time. We propose a domain-specific language for writing properties, called Indus, and we develop a compiler that turns properties thus specified into executable P4 code that runs alongside the forwarding code at line rate. To evaluate our approach, we used Indus to model a range of properties, showing that it is expressive enough to capture examples studied in prior work. We also deployed Hydra checkers for validating paths in source routing and for enforcing slice isolation in Aether, an open-source cellular platform. We confirmed a subtle bug in Aether's 5G mobile core that would have been hard to detect using static techniques. We also evaluated the overheads of Hydra on hardware, finding that it does not significantly increase latency and often does not require additional pipeline stages. 

There has been great progress in soft robot design, manufacture, and control in recent years, and soft robots are a tool of choice for safe and robust handling of objects in conditions of uncertainty. Still, dexterous in-hand manipulation using soft robots remains a challenge. This paper introduces foam robot hands actuated by tendons sewn through a fabric glove. The flexibility of tendon actuation allows for high competence in utilizing deformation for robust in-hand manipulation. We discuss manufacturing, control, and design optimization for foam robots and demonstrate robust grasping and in-hand manipulation on a variety of different physical hand prototypes.